(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/types.ma".
include "basics/bool.ma".
include "arithmetics/nat.ma".

(* ------------------ *)
definition empty_set ≝ λA:Type[0].λa:A.False.
interpretation "empty set" 'empty_set = (empty_set ?).
notation "\emptyv" 
   non associative with precedence 90 for @{'empty_set}.

(* check (empty_set nat). *)

definition singleton ≝ λA.λx,a:A.x=a.
interpretation "singleton" 'singleton x = (singleton ? x).
notation "⦃x⦄" 
  non associative with precedence 90 for @{'singleton $x}.

(* check (singleton nat 0). *)

definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
interpretation "complement" 'complement a = (complement ? a).
notation "¬ x" 
  non associative with precedence 90 for @{'complement $x}.

definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
interpretation "union" 'union a b = (union ?? a b).
notation "hvbox(a break ∪ b)"
  right associative with precedence 47 for @{'union $a $b}.

definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
interpretation "intersection" 'intersection a b = (intersection ? a b).
notation "hvbox(a break ∩ b)"
  right associative with precedence 47 for @{'intersection $a $b}.

definition setminus := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
interpretation "setminus" 'setminus a b = (setminus ? a b).
notation "hvbox(a break ∖  b)"
  right associative with precedence 80 for @{'setminus $a $b}.

(* Finally, we use implication to define the inclusion relation between
sets *)

definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
interpretation "subset" 'subseteq a b = (subset ? a b).


(* ---------- *)
definition Set357 ≝ (union nat ⦃3⦄  (union nat ⦃5⦄  ⦃7⦄)).
definition Set579 ≝ (union nat ⦃5⦄  (union nat ⦃7⦄  ⦃9⦄)).


let rec add n m ≝ match n with [ O ⇒ m | S a ⇒ S (add a m)].

definition twice ≝ λn.add n n. 

definition set_of_even ≝ λn. ∃m. n = (twice m) .

definition set_of_odd ≝ λn. ∃m. n = S (twice m) .

definition set_of_nats ≝ union nat set_of_even  set_of_odd .

lemma pp : ∀ n:nat. n 




(* ---------------- *)
inductive ES (A:Type[0]) : Prop ≝
    mkES: ES A .
notation "\emptyv" non associative with precedence 90 for @{'ES}.
interpretation "Empty Set" 'ES = (ES ?).

inductive Sing (A:Type[0]) (a:A) : Prop ≝
    mkSing: Sing A a.
    
notation "⦃x⦄" non associative with precedence 90 for @{'Sing $x}.
interpretation "Singleton" 'Sing x = (Sing ? x).
    
inductive Uni (A:Type[0]) (B:Type[0]) (a:A) (b:B) : Prop ≝
    mkUni: Uni A B a b.
    
notation "hvbox(a break ∪b)"
  right associative with precedence 47
  for @{'mkUni $a $b}.
interpretation "Uni" 'Uni a b = (Uni ?? a b).
  
(* 
   check ⦃S(0)⦄.
   check (Uni (Sing nat (S(0))) (Sing nat (S(0))) ) 
   check (Uni ⦃S(0)⦄ ⦃S(0)⦄ ). 
   check (Uni ⦃S(0)⦄ ∅ ) . 
*)
